/*
 * BooleanVectorTest.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <gtest/gtest.h>

#include "bfr/BooleanVector.hpp"
#include "bfr/Literal.hpp"
#include "bfr/Clause.hpp"

namespace bfr { namespace test {

TEST(BooleanVector, basics) {
    BooleanVector v;
    v.push_back(0);
    v.push_back(1);
    v.push_back(0);
    EXPECT_EQ("(0, 1, 0)", v.asString());
    EXPECT_EQ(3, v.size());
    v[1] = 0;
    v[2] = 1;
    EXPECT_EQ("(0, 0, 1)", v.asString());
}

TEST(BooleanVector, equals) {
    BooleanVector v1;
    v1.append(4, true, true, false, false);

    BooleanVector v2;
    v2.append(4, true, true, false, false);

    EXPECT_EQ(v1, v2);

    BooleanVector v3;
    v3.append(4, true, true, false, true);
    EXPECT_NE(v1, v3);
}

TEST(BooleanVector, hull) {
    // (1, 0, 0, 1, 1)
    // (1, 1, 0, 1, 0)
    BooleanVector v1;
    v1.push_back(true);
    v1.push_back(false);
    v1.push_back(false);
    v1.push_back(true);
    v1.push_back(true);

    BooleanVector v2;
    v2.push_back(true);
    v2.push_back(true);
    v2.push_back(false);
    v2.push_back(true);
    v2.push_back(false);
    Clause *result = v1.getHull(v2);
    Clause expected;
    expected.add(new Literal(0));
    expected.add(new Literal(2, false));
    expected.add(new Literal(3));

    EXPECT_EQ(expected, *result);
    Clause *result2 = v2.getHull(v1);
    EXPECT_EQ(*result, *result2);
    delete result;
    delete result2;
}

} // namespace test
} // namespace bfr


